#include "PDTNot.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"

PDTNot::PDTNot(PDTCodeGraph & CG, PDTExpBool &operand) :
  PDTExpBoolUn(CG, operand)
{

}

Z3_ast
PDTNot::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  if (Z3node != NULL)
    return Z3node;

  Z3_ast child = children[0]->Z3visit(ZV);

  Z3node = Z3_mk_not(ZV.ctx, child);

  return Z3node;
}
